| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), Consistent(R;es), Type, MaInterface(T), IdLnk, Id, Namer(n;Id_list), Normal(A,I), gluable(I;l;tg), gluable2(A;I;l;tg), R-Feasible(R), ES, interfaceGlue(A; I; l; tg; nmr), Realizer,  , ma-interface-glued-p(es;A;I;l;tg), P   Q,  x.A(x), x:A  B(x),  b, a:A fp B(a), Atom$n, {x:A| B(x)} , ma-interface-valtype(I;i;k), xdom(f). v=f(x) P(x;v), P & Q, Normal(T), Normal(ds), False,  A, f(a), t.1, x : v, f  g, es realizer ind, ma-interface-tags(I), [], lname(l), [car / cdr], as @ bs, #$n,  ,  es.P(es),  x. t(x), xL.R(x), A  B,  , Outcome, a < b, Void,  , strong-subtype(A;B),  , S  T, type List, A List , IdDeq, f(x), t.2, ma-interface-ds(I;i), source(l), (link n from i to j), triggers-glued-p(es; A; l; tg; ds; conds), ma-interface-locs(I), remove-repeats(eq;L), a = b,  b, filter(P;l), xL. P(x), p  q, p  q, p q, deq-member(eq;x;L), (x l), P  Q, ma-interface-dom(I;i), Knd, hasloc(k;i), State(ds), left + right, Top, A c B,  x:A. B(x), x dom(f), fpf-domain(f), EqDecider(T), P Q, glued(es; B; f; Ia; Ib), es-triggers(es;i;ds;conds), valtype(e), E, es-triggers-params-consistent(es;A;i;ds;conds), es-realizer(p), |g|, ||as||, i j < k, ma-interface-info(I;i;k), {i..j }, s ~ t, SQType(T), l[i], last(L), hd(l), P Q, kind(e), left right, (L), triggersGlue(A; l; tg; ds; conds), ma-interface-loc(I;i),  , (L), mapl(f;l), ma-interface-conds(I;i), es-in-port-conds(A;l;tg), rec(x.A(x)), DeclaredType(ds;x), FinProbSpace, Unit, Rplus-left(x1), es realizer ind Rnone compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rbframe compseq tag def, Rplus?(x1), Rplus-right(x1), es realizer ind Rrframe compseq tag def, A B,  x:A.B(x),  T, True, {T}, State(ds), Interface(ds;da;A), state@i, vartype(i;x), loc(e), f(x)?z, f g, triggers-glued-realizable, rcv(l,tg), KindDeq, R ||- es.P(es), let x,y = A in B(x;y), lsrc mk lnk compseq tag def, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), <a, b>, Inj(A;B;f), tag(k), tag_rcv{tag_rcv_compseq_tag_def:ObjectId}(tg; l), isrcv(k), isrcvl(l;k), isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), locl(a),  , ff, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, tt, dt(l;da), x(s1,s2), x,y. t(x;y), (xL.P(x)), lnk(k), destination(l), a = b, x(s), (x,yL. P(x;y)), no_repeats(T;l), IsPrimeIdeal(R;P), IsIntegDom(r), a b, IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P), f2f+-pred(e',e), [e: i  p j], [e: i p j], same-thread(es;p;e;e'), es-r-immediate-pred(es;R;e';e), e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), e c e', (e < e'), e loc e' , (e <loc e'), MaName, l_disjoint(T;l1;l2), Dec(P), i  j , n+m, f || g, map(f;as), es-first-from(es;e;l;tg), isrcv(e), lnk(e), tag(e), E(X), X(e), es-in-port(es;l;tg), glues(es; B; g; f; Ia; Ib), g glues Ia:Qa f Ib:Rb, kind(e), loc(e), constant_function(f;A;B), r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), EState(T), EOrderAxioms(E; pred?; info), discrete state@i, Decision, inl x , ma-interface-consistent2(es;I), e@i. P(e), AbsInterface(A), p-first(L), ma-interface-domb(I;i;k), ma-interface-consistent(es;X), [[X]], [[I|]], e X, ma-interface-consistent-at(es;i;X), inr x , q-rel(r;x), r < s, a < b, a <p b, a b, a ~ b, b | a, f o g, if a=1 b then x else y, (last change to x before e), X Y = 0, [[I|i]], can-apply(f;x), ma-interface-code(I;i;k), y is f*(x), lnk-inv(l), es-init(es;e), lastchange(x;e), suptype(S; T), val(e), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), ldst mk lnk compseq tag def, Q = f== P, f is Q-R-pre-preserving on P |
| Lemmas | glues wf, es-in-port wf, glued-composes, it wf, es-kind-rcv, es-val wf, es-is-interface-p-first, glued-to-self, ma-interface-subtype, es-is-interface-ma-interface-triggers, ma-interface-triggers-val, es-isrcv-loc, int seg properties, es-loc-pred, select-map, length-map, ma-interface-triggers-loc, ma-interface-triggers wf, glued-first, es-interface-disjoint wf, map-map, subtype rel sum, decidable assert, decidable wf, es-is-interface wf, btrue wf, es-interface wf, ma-interface-triggers-list wf, p-first wf-interface, p-first wf, es-E-interface wf, es-interface-val wf, ma-abs-interface wf, ma-interface-consistent wf, ma-interface-consistent-consistent2, ma-interface-triggers-list-p-first, ma-interface-domb wf, assert-ma-interface-domb, alle-at wf, ma-interface-consistent2 wf, fpf-compatible-singles, fpf-single-dom, fpf-compatible-symmetry, pairwise-mapl-no-repeats, ldst wf, es-state-type-implies, es-state-subtype, es-state-subtype-iff, es-vartype wf, deq wf, EOrderAxioms wf, EState wf, kindcase wf, Msg wf, val-axiom wf, cless wf, qle wf, constant function wf, es-tag wf, es-lnk wf, es-rcv-kind, es-triggers-p-first, map wf, map wf3, fpf-compatible wf, non neg length, select member, decidable equal Id, decidable l member, sq stable from decidable, and functionality wrt iff, or functionality wrt iff, assert of bor, remove-repeats property, no-repeats-pairwise, pairwise-map2, pairwise wf, fpf-join-list-ap-disjoint, es-loc wf, es-state wf, l exists wf, cons member, rcv one one, member singleton, fpf-join-list-domain, bfalse wf, eq knd wf, bor wf, assert-deq-member, deq-member wf, fpf-join-list-ap, fpf-all-empty, assert-hasloc, assert-eq-knd, fpf-single-dom-sq, bool sq, bool cases, member-mapl, fpf-join-list-dom2, R-sub-plus-right3, length wf1, mapl wf, fpf-join-list wf, implies functionality wrt iff, all functionality wrt iff, fpf-all wf, fpf-empty-sub, fpf-sub wf, subtype-fpf-cap-top, fpf-cap wf, subtype rel self, subtype rel dep function, es-in-port-conds wf, Id sq, ma-interface-conds wf, ma-interface-conds wf2, ifthenelse wf, ma-interface-conds wf3, rev implies wf, iff wf, eqtt to assert, eqff to assert, ma-interface-loc wf, fpf-empty wf, assert-ma-interface-loc, es-kind wf, subtype-fpf2, isrcv wf, ma-interface-tags-property2, member append, ma-interface-dom-hasloc, member-fpf-domain, subtype-set-hasloc, subtype rel set, subtype rel function, subtype rel list, subtype rel product, squash wf, true wf, R-sub-plus-left, es realizer wf, bool wf, finite-prob-space wf, decl-type wf, rationals wf, unit wf, false wf, Kind-deq wf, l member subtype, Knd sq, guard wf, int seg wf, mk lnk wf, rcv wf, pi1 wf, fpf-dom wf, triggersGlue wf, R-realizes wf, select wf, fpf-domain wf, length wf nat, normal-ds wf, R-sub-Rall2, R-sub wf, R-sub-implies, triggers-glued-realizable, es-E wf, es-valtype wf, glued wf, es-triggers wf, es-triggers-params-consistent wf, fpf-trivial-subtype-top, fpf wf, Knd wf, decl-state wf, top wf, subtype rel wf, member-fpf-dom, fpf-ap wf, hasloc wf, ma-interface-dom wf, normal-type wf, ma-interface-valtype wf, member-remove-repeats, assert wf, not wf, lsrc wf, eq id wf, bnot wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, member filter, ma-interface-locs wf, id-deq wf, remove-repeats wf, filter wf, l member wf, triggers-glued-p wf, ma-interface-ds wf, l all wf, es-real wf, gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, append wf, lname wf, ma-interface-tags wf, nat wf, member wf, le wf, Id wf, IdLnk wf, ma-interface wf, interfaceGlue wf, interfaceGlue feasible, implies-es-real, event system wf, ma-interface-glued-p wf, R-consistent wf |